#include <signal.h>
#include "ic3/ic3.h"
#include "util/util.h"
#include "base/aig.h"
#include "util/usage.h"

static Usage usg;

static void report()
{
   extern void print_prof();

   usg.report();
   print_prof();
}
static void mySIGINT_handler( int )
{
   cout << "undecidable" <<endl;
   report();
   exit(1);
}

int main( int argc , const char ** argv )
{
   signal(SIGALRM, mySIGINT_handler);
   signal(SIGINT, mySIGINT_handler);
   signal(SIGTERM, mySIGINT_handler);

   ArgAnalyzer arg( "prove <ckt:aig>" , argc , argv );
   StrashAIG ckt;
   ckt.read_aig( arg[0].c_str() );
   IC3 ic3;
   if( ic3.init( ckt ) )
   { 
      cout << "cex"<< endl; 
      return 0;
   }
   if( ic3.prove() ) 
   {
      ic3.ic3info();
      cout << "prove"<< endl;
   }
   else
   {
      ic3.ic3info();
      cout << "cex" << endl;
   }
   report();
}
